the_es:ES, e, e':E. Dec(e = e') 

latex

Definitions	ES, P  Q, P & Q, P  Q, P  Q, E, Prop, b, t  T, e = e', Dec(P), x:A. B(x)
Lemmas	decidable assert, es-eq-E wf, assert wf, assert-es-eq-E, decidable functionality, event system wf, es-E wf